Computer programs and software are ubiquitous and are used not just to direct the functionality of conventional computers but also to control and enhance the functionality of a myriad of modern products and appliances. For instance, televisions, household appliances, cellular phones, automobiles, medical devices, and so forth, may incorporate computer programs which direct and enhance their functionality. The theoretical and practical analysis of computer programs is an important aspect of software research, development, modification, enhancement, and maintenance. The ability to analyze computer programs and reason about their execution, from both theoretical and practical perspectives, aids software developers by allowing them to make better and more informed choices during development of software and the modification or enhancement of existing software. Analysis of software is useful for proving correctness of code, for performing optimizations of existing code, for doing performance analysis and so on.
Computers and computer processors are no longer simple single processors executing software in an instruction-by-instruction sequential fashion. The availability of multi-core processors is increasing and the demand for concurrent (or parallel) software to take advantage of multi-processor computers and multi-core processors is also increasing. Computers are increasingly having multiple processors that can concurrently, or in parallel, execute multiple instructions and procedure threads simultaneously. Such concurrent processing (also referred to as “parallelism”) can greatly increase both the speed and processing power of computer systems when correctly exploited.
This increasing availability of multi-core processors and multiple processor computers is rapidly increasing the availability of parallelism in computing hardware and is increasing the demand on developers to develop and redesign software to exploit that parallelism. The use of parallelism and concurrency in programming is becoming increasingly more useful, important, and ubiquitous. However, analysis and verification of concurrent software can be extremely difficult, and determining properties for the software and checking their correctness can be problematic for software developers and computer scientists.
For purposes of analysis, it is often efficient and desirable to reduce the complexity of the software using some abstraction, eliminating aspects not necessary for the analysis. For sequential programs, abstracting only data was often a sufficient basis for analysis. For concurrent programs, however, abstraction of data, alone, is not enough. During execution of a concurrent program, there may be multiple threads operating on the same data simultaneously. For the analysis of concurrent programs, it is desirable to abstract program control (as well as, possibly, data).
Because of the greater information necessary in the analysis of concurrent programs, analysis of parallel or concurrent programs is hard—theoretically as well as practically. For sequential programs, intraprocedural analysis using a regular language abstraction may be accomplished in P-time. Interprocedural analysis using a context-free language abstraction for a sequential program may also be accomplished in P-time. However, the intraprocedural analysis using a regular language abstraction in a concurrent program is PSPACE-hard and the interprocedural analysis using context-free language abstraction is theoretically undecidable.
Because of the difficulties encountered in using more common abstraction techniques, better methods are needed for the abstraction and analysis of parallel or concurrent software. When two or more threads of a program may be executing simultaneously, then the possible states for the program may be given by the cross product of all the possible states of one thread with the possible states of the other executing threads. For concurrent programs with a reasonably large number of states within a single thread or large numbers of threads, this number of possible states may be huge. The huge number of program control states possible in concurrent programs makes abstraction of concurrent programs, and their analysis, a difficult problem.
Flow-insensitive pointer analysis for concurrent programs, which analyzes the states of data but ignores the states of the program flow or control, can be efficient but is imprecise. Flow-sensitive analysis, which takes into account the program control states of independently executing threads of a concurrent program, can be precise but is inefficient.